YES 1.555
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((notElem :: Eq a => [a] -> [[a]] -> Bool) :: Eq a => [a] -> [[a]] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((notElem :: Eq a => [a] -> [[a]] -> Bool) :: Eq a => [a] -> [[a]] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (notElem :: Eq a => [a] -> [[a]] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2700), Succ(xv4000000)) → new_primPlusNat(xv2700, xv4000000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2700), Succ(xv4000000)) → new_primPlusNat(xv2700, xv4000000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30000), Succ(xv400000)) → new_primMulNat(xv30000, Succ(xv400000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30000), Succ(xv400000)) → new_primMulNat(xv30000, Succ(xv400000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_@2, bdb), bdc)), bce)) → new_esEs3(xv300, xv4000, bdb, bdc)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(app(ty_Either, bg), bh)) → new_esEs1(xv302, xv4002, bg, bh)
new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(ty_[], hc))) → new_esEs(xv300, xv4000, hc)
new_esEs1(Left(xv300), Left(xv4000), app(app(app(ty_@3, fa), fb), fc), fd) → new_esEs0(xv300, xv4000, fa, fb, fc)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, ee), bc, da) → new_esEs2(xv300, xv4000, ee)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(ty_Maybe, ca)) → new_esEs2(xv302, xv4002, ca)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_[], bda)), bce)) → new_esEs(xv300, xv4000, bda)
new_esEs1(Right(xv300), Right(xv4000), gd, app(app(app(ty_@3, ge), gf), gg)) → new_esEs0(xv300, xv4000, ge, gf, gg)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], bda), bce) → new_esEs(xv300, xv4000, bda)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, bcb), bcc), bcd), bce) → new_esEs0(xv300, xv4000, bcb, bcc, bcd)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_Either, ff), fg), fd) → new_esEs1(xv300, xv4000, ff, fg)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(ty_[], cb)) → new_esEs(xv302, xv4002, cb)
new_esEs2(Just(xv300), Just(xv4000), app(ty_Maybe, bac)) → new_esEs2(xv300, xv4000, bac)
new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_Maybe, fh)), fd)) → new_esEs2(xv300, xv4000, fh)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(app(ty_Either, db), dc), da) → new_esEs1(xv301, xv4001, db, dc)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(ty_[], bbg))) → new_esEs(xv301, xv4001, bbg)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_@2, eg), eh)), bc), da)) → new_esEs3(xv300, xv4000, eg, eh)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(ty_[], bbg)) → new_esEs(xv301, xv4001, bbg)
new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_[], ga)), fd)) → new_esEs(xv300, xv4000, ga)
new_esEs2(Just(xv300), Just(xv4000), app(app(app(ty_@3, hf), hg), hh)) → new_esEs0(xv300, xv4000, hf, hg, hh)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, eg), eh), bc, da) → new_esEs3(xv300, xv4000, eg, eh)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(app(app(ty_@3, ce), cf), cg)), da)) → new_esEs0(xv301, xv4001, ce, cf, cg)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_Maybe, bch)), bce)) → new_esEs2(xv300, xv4000, bch)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(ty_[], de), da) → new_esEs(xv301, xv4001, de)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(app(ty_Either, bbd), bbe))) → new_esEs1(xv301, xv4001, bbd, bbe)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, bdb), bdc), bce) → new_esEs3(xv300, xv4000, bdb, bdc)
new_esEs1(Left(xv300), Left(xv4000), app(ty_Maybe, fh), fd) → new_esEs2(xv300, xv4000, fh)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(app(app(ty_@3, bd), be), bf))) → new_esEs0(xv302, xv4002, bd, be, bf)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_Either, bcf), bcg)), bce)) → new_esEs1(xv300, xv4000, bcf, bcg)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(app(ty_@3, bcb), bcc), bcd)), bce)) → new_esEs0(xv300, xv4000, bcb, bcc, bcd)
new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(app(app(ty_@3, ge), gf), gg))) → new_esEs0(xv300, xv4000, ge, gf, gg)
new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_Maybe, bac))) → new_esEs2(xv300, xv4000, bac)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs0(xv301, xv4001, bba, bbb, bbc)
new_esEs1(Right(xv300), Right(xv4000), gd, app(ty_[], hc)) → new_esEs(xv300, xv4000, hc)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(ty_Maybe, ca))) → new_esEs2(xv302, xv4002, ca)
new_esEs1(Right(xv300), Right(xv4000), gd, app(ty_Maybe, hb)) → new_esEs2(xv300, xv4000, hb)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(ty_[], cb))) → new_esEs(xv302, xv4002, cb)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_@2, gb), gc), fd) → new_esEs3(xv300, xv4000, gb, gc)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(ty_[], de)), da)) → new_esEs(xv301, xv4001, de)
new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_Either, ff), fg)), fd)) → new_esEs1(xv300, xv4000, ff, fg)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(app(ty_@2, df), dg)), da)) → new_esEs3(xv301, xv4001, df, dg)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(app(ty_@2, cc), cd)) → new_esEs3(xv302, xv4002, cc, cd)
new_esEs2(Just(xv300), Just(xv4000), app(ty_[], bad)) → new_esEs(xv300, xv4000, bad)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(app(ty_@2, bbh), bca))) → new_esEs3(xv301, xv4001, bbh, bca)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, bcf), bcg), bce) → new_esEs1(xv300, xv4000, bcf, bcg)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(ty_Maybe, bbf)) → new_esEs2(xv301, xv4001, bbf)
new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(ty_Maybe, hb))) → new_esEs2(xv300, xv4000, hb)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_[], ef)), bc), da)) → new_esEs(xv300, xv4000, ef)
new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_@2, bae), baf))) → new_esEs3(xv300, xv4000, bae, baf)
new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(app(ty_@3, fa), fb), fc)), fd)) → new_esEs0(xv300, xv4000, fa, fb, fc)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, ec), ed), bc, da) → new_esEs1(xv300, xv4000, ec, ed)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_Either, ec), ed)), bc), da)) → new_esEs1(xv300, xv4000, ec, ed)
new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(app(ty_@2, hd), he))) → new_esEs3(xv300, xv4000, hd, he)
new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_[], bad))) → new_esEs(xv300, xv4000, bad)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(app(ty_@2, cc), cd))) → new_esEs3(xv302, xv4002, cc, cd)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(app(app(ty_@3, ce), cf), cg), da) → new_esEs0(xv301, xv4001, ce, cf, cg)
new_esEs1(Right(xv300), Right(xv4000), gd, app(app(ty_Either, gh), ha)) → new_esEs1(xv300, xv4000, gh, ha)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(app(ty_@2, df), dg), da) → new_esEs3(xv301, xv4001, df, dg)
new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_@2, gb), gc)), fd)) → new_esEs3(xv300, xv4000, gb, gc)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(app(ty_@2, bbh), bca)) → new_esEs3(xv301, xv4001, bbh, bca)
new_esEs2(Just(xv300), Just(xv4000), app(app(ty_Either, baa), bab)) → new_esEs1(xv300, xv4000, baa, bab)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], ef), bc, da) → new_esEs(xv300, xv4000, ef)
new_esEs(:(xv30, xv31), :(xv400, xv401), ba) → new_esEs(xv31, xv401, ba)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, bch), bce) → new_esEs2(xv300, xv4000, bch)
new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(app(ty_Either, bbd), bbe)) → new_esEs1(xv301, xv4001, bbd, bbe)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(app(app(ty_@3, bd), be), bf)) → new_esEs0(xv302, xv4002, bd, be, bf)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(app(ty_Either, bg), bh))) → new_esEs1(xv302, xv4002, bg, bh)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(app(app(ty_@3, bba), bbb), bbc))) → new_esEs0(xv301, xv4001, bba, bbb, bbc)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_Maybe, ee)), bc), da)) → new_esEs2(xv300, xv4000, ee)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(ty_Maybe, bbf))) → new_esEs2(xv301, xv4001, bbf)
new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_Either, baa), bab))) → new_esEs1(xv300, xv4000, baa, bab)
new_esEs2(Just(xv300), Just(xv4000), app(app(ty_@2, bae), baf)) → new_esEs3(xv300, xv4000, bae, baf)
new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(app(ty_@3, hf), hg), hh))) → new_esEs0(xv300, xv4000, hf, hg, hh)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(ty_Maybe, dd)), da)) → new_esEs2(xv301, xv4001, dd)
new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(app(ty_Either, gh), ha))) → new_esEs1(xv300, xv4000, gh, ha)
new_esEs1(Left(xv300), Left(xv4000), app(ty_[], ga), fd) → new_esEs(xv300, xv4000, ga)
new_esEs1(Right(xv300), Right(xv4000), gd, app(app(ty_@2, hd), he)) → new_esEs3(xv300, xv4000, hd, he)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(app(ty_@3, dh), ea), eb)), bc), da)) → new_esEs0(xv300, xv4000, dh, ea, eb)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(app(ty_Either, db), dc)), da)) → new_esEs1(xv301, xv4001, db, dc)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(ty_Maybe, dd), da) → new_esEs2(xv301, xv4001, dd)
new_esEs(:(xv30, xv31), :(xv400, xv401), app(ty_[], bag)) → new_esEs(xv30, xv400, bag)
new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, dh), ea), eb), bc, da) → new_esEs0(xv300, xv4000, dh, ea, eb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(Just(xv300), Just(xv4000), app(ty_[], bad)) → new_esEs(xv300, xv4000, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(xv300), Just(xv4000), app(app(app(ty_@3, hf), hg), hh)) → new_esEs0(xv300, xv4000, hf, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(xv300), Just(xv4000), app(app(ty_Either, baa), bab)) → new_esEs1(xv300, xv4000, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xv300), Just(xv4000), app(app(ty_@2, bae), baf)) → new_esEs3(xv300, xv4000, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xv300), Just(xv4000), app(ty_Maybe, bac)) → new_esEs2(xv300, xv4000, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], bda), bce) → new_esEs(xv300, xv4000, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(ty_[], bbg)) → new_esEs(xv301, xv4001, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, bcb), bcc), bcd), bce) → new_esEs0(xv300, xv4000, bcb, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs0(xv301, xv4001, bba, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, bcf), bcg), bce) → new_esEs1(xv300, xv4000, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(app(ty_Either, bbd), bbe)) → new_esEs1(xv301, xv4001, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, bdb), bdc), bce) → new_esEs3(xv300, xv4000, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(app(ty_@2, bbh), bca)) → new_esEs3(xv301, xv4001, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), bah, app(ty_Maybe, bbf)) → new_esEs2(xv301, xv4001, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, bch), bce) → new_esEs2(xv300, xv4000, bch)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(xv300), Right(xv4000), gd, app(ty_[], hc)) → new_esEs(xv300, xv4000, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(xv300), Left(xv4000), app(ty_[], ga), fd) → new_esEs(xv300, xv4000, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(ty_[], hc))) → new_esEs(xv300, xv4000, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_[], bda)), bce)) → new_esEs(xv300, xv4000, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(ty_[], bbg))) → new_esEs(xv301, xv4001, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_[], ga)), fd)) → new_esEs(xv300, xv4000, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(ty_[], cb))) → new_esEs(xv302, xv4002, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(ty_[], de)), da)) → new_esEs(xv301, xv4001, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_[], ef)), bc), da)) → new_esEs(xv300, xv4000, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_[], bad))) → new_esEs(xv300, xv4000, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xv30, xv31), :(xv400, xv401), ba) → new_esEs(xv31, xv401, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(xv30, xv31), :(xv400, xv401), app(ty_[], bag)) → new_esEs(xv30, xv400, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(ty_[], cb)) → new_esEs(xv302, xv4002, cb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(ty_[], de), da) → new_esEs(xv301, xv4001, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], ef), bc, da) → new_esEs(xv300, xv4000, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(xv300), Left(xv4000), app(app(app(ty_@3, fa), fb), fc), fd) → new_esEs0(xv300, xv4000, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Right(xv300), Right(xv4000), gd, app(app(app(ty_@3, ge), gf), gg)) → new_esEs0(xv300, xv4000, ge, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(Left(xv300), Left(xv4000), app(app(ty_Either, ff), fg), fd) → new_esEs1(xv300, xv4000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xv300), Right(xv4000), gd, app(app(ty_Either, gh), ha)) → new_esEs1(xv300, xv4000, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Left(xv300), Left(xv4000), app(app(ty_@2, gb), gc), fd) → new_esEs3(xv300, xv4000, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xv300), Right(xv4000), gd, app(app(ty_@2, hd), he)) → new_esEs3(xv300, xv4000, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Left(xv300), Left(xv4000), app(ty_Maybe, fh), fd) → new_esEs2(xv300, xv4000, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(xv300), Right(xv4000), gd, app(ty_Maybe, hb)) → new_esEs2(xv300, xv4000, hb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(app(app(ty_@3, ce), cf), cg)), da)) → new_esEs0(xv301, xv4001, ce, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(app(app(ty_@3, bd), be), bf))) → new_esEs0(xv302, xv4002, bd, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(app(ty_@3, bcb), bcc), bcd)), bce)) → new_esEs0(xv300, xv4000, bcb, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(app(app(ty_@3, ge), gf), gg))) → new_esEs0(xv300, xv4000, ge, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(app(ty_@3, fa), fb), fc)), fd)) → new_esEs0(xv300, xv4000, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(app(app(ty_@3, bba), bbb), bbc))) → new_esEs0(xv301, xv4001, bba, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(app(ty_@3, hf), hg), hh))) → new_esEs0(xv300, xv4000, hf, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(app(ty_@3, dh), ea), eb)), bc), da)) → new_esEs0(xv300, xv4000, dh, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(app(app(ty_@3, ce), cf), cg), da) → new_esEs0(xv301, xv4001, ce, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(app(app(ty_@3, bd), be), bf)) → new_esEs0(xv302, xv4002, bd, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, dh), ea), eb), bc, da) → new_esEs0(xv300, xv4000, dh, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(app(ty_Either, bbd), bbe))) → new_esEs1(xv301, xv4001, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_Either, bcf), bcg)), bce)) → new_esEs1(xv300, xv4000, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_Either, ff), fg)), fd)) → new_esEs1(xv300, xv4000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_Either, ec), ed)), bc), da)) → new_esEs1(xv300, xv4000, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(app(ty_Either, bg), bh))) → new_esEs1(xv302, xv4002, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_Either, baa), bab))) → new_esEs1(xv300, xv4000, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(app(ty_Either, gh), ha))) → new_esEs1(xv300, xv4000, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(app(ty_Either, db), dc)), da)) → new_esEs1(xv301, xv4001, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_@2, bdb), bdc)), bce)) → new_esEs3(xv300, xv4000, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_@2, eg), eh)), bc), da)) → new_esEs3(xv300, xv4000, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(app(ty_@2, df), dg)), da)) → new_esEs3(xv301, xv4001, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(app(ty_@2, bbh), bca))) → new_esEs3(xv301, xv4001, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_@2, bae), baf))) → new_esEs3(xv300, xv4000, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(app(ty_@2, hd), he))) → new_esEs3(xv300, xv4000, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(app(ty_@2, cc), cd))) → new_esEs3(xv302, xv4002, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_@2, gb), gc)), fd)) → new_esEs3(xv300, xv4000, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_Maybe, fh)), fd)) → new_esEs2(xv300, xv4000, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_Maybe, bch)), bce)) → new_esEs2(xv300, xv4000, bch)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_Maybe, bac))) → new_esEs2(xv300, xv4000, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), bc), app(ty_Maybe, ca))) → new_esEs2(xv302, xv4002, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gd), app(ty_Maybe, hb))) → new_esEs2(xv300, xv4000, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_Maybe, ee)), bc), da)) → new_esEs2(xv300, xv4000, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, bah), app(ty_Maybe, bbf))) → new_esEs2(xv301, xv4001, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bb), app(ty_Maybe, dd)), da)) → new_esEs2(xv301, xv4001, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(app(ty_Either, bg), bh)) → new_esEs1(xv302, xv4002, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(app(ty_Either, db), dc), da) → new_esEs1(xv301, xv4001, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, ec), ed), bc, da) → new_esEs1(xv300, xv4000, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, eg), eh), bc, da) → new_esEs3(xv300, xv4000, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(app(ty_@2, cc), cd)) → new_esEs3(xv302, xv4002, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(app(ty_@2, df), dg), da) → new_esEs3(xv301, xv4001, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, ee), bc, da) → new_esEs2(xv300, xv4000, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, bc, app(ty_Maybe, ca)) → new_esEs2(xv302, xv4002, ca)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bb, app(ty_Maybe, dd), da) → new_esEs2(xv301, xv4001, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3